Model checking techniques are widely used in design verification of complex hardware systems and, to a lesser extent, in verification of software programs. In model checking, a test engineer specifies properties that the system under design is expected to fulfill. The model checker then verifies that there is no reachable state of the system that will violate the property, or else it finds a counterexample, i.e., an input sequence and succession of state transitions in the model that lead to violation of one of the properties.
A variety of techniques are known in the art for carrying out this sort of model checking. One well-known technique is bounded model checking (BMC), in which the system under design and the property to be verified are represented as Boolean formulas. The model checker attempts to find a counterexample by applying a propositional satisfiability (SAT) technique to the conjunction of the Boolean formulas. BMC considers only counterexamples up to a particular depth K (i.e., extending over K steps of the transition relation of the system), and generates a propositional formula that is satisfiable if and only if a counterexample exists. Various methods of automatic SAT solving that may be used in this context are known in the art. Some representative methods are described, for example, in U.S. Pat. No. 7,047,139, whose disclosure is incorporated herein by reference.
Although BMC has been used mainly in verification of hardware designs, a number of BMC-based software verification techniques have been developed. Techniques of this sort are described, for example, in U.S. Patent Application publications US 2004/0019468 A1 and US 2005/0166167 A1, whose disclosures are incorporated herein by reference.
In some applications of BMC, the Boolean formula representing the system under design may be transformed into a static single assignment (SSA) form. For example, U.S. Patent Application Publication US 2005/0071147 A1, whose disclosure is incorporated herein by reference, describes a method for verifying a circuit design using a SAT solver that operates on a SSA representation of a C-language program. The SSA form, which is well known in the art, and a method for its computation are described by Cytron et al., in “An Efficient Method of Computing Static Single Assignment Form,” Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (ACM Press, 1989), pages 25-35, which is incorporated herein by reference.
Even if the SAT solver used in BMC is unable to find a counterexample in K steps, there may still be a state of the system that is reachable in a greater number of steps and violates the specified property. A number of methods have been proposed to enable the SAT solver to cover all reachable states of the system by successive over-approximations of the state space, and thus to verify that the property is satisfied on all states. For example, U.S. Pat. No. 6,944,838, whose disclosure is incorporated herein by reference, describes a design verifier that includes a bounded model checker, a proof partitioner and a fixed-point detector. If the bounded model checker does not find a counterexample at some depth K, the proof partitioner provides an over-approximation of the states that are reachable in one or more steps using a proof generated by the bounded model checker. (This sort of over-approximation is commonly known as a Craig interpolant.) The fixed-point detector detects whether the over-approximation is at a fixed point. If so, the design is verified.